open Bigarray

(*********************************************************************)
(* Graph provides graph manipulation operations that are specialized *)
(* for automata theory                                               *)
(*********************************************************************)
module Int = struct
	type t = int
	let compare = compare
end
module IntSet = Set.Make(Int);;
module IntMap = Map.Make(Int);;

module Int2 = struct
	type t = int * int
	let compare = compare
end
module Int2Set = Set.Make(Int2);;
module Int2Map = Map.Make(Int2);;

(* a set that contains sets of vertices *)
module PIntSet = Set.Make(IntSet);;

(* All-Pairs Shortest Paths: to find a cycle in a graph *)
(* n: number of vertices
	matrix: cell (i,j) is
		1, if there is an edge from vi to vj
		max_int, otherwise
*)
let print n dist last =
	begin
		for i = 0 to n-1 do
			for j = 0 to n-1 do
				if dist.{!last,i,j}=max_int then
					print_string ("~ ")
				else
					print_string ((string_of_int dist.{!last,i,j})^" ")
			done;
			print_endline ""
		done;
		print_endline "\n\n";
	end


let floyd_warshall n matrix =
	let dist = Array3.create int c_layout 2 n n in  (* two arrays: (v1,v2) -> distance *)
	let prior = Array3.create int c_layout 2 n n in  (* two arrays: (v1,v2) -> v_between *)
	let last = ref 0 in
	begin
		(* init dist.{0} and prior.{0} *)
		for i = 0 to n-1 do
			for j = 0 to n-1 do
				dist.{0,i,j} <- matrix.{i,j};
				prior.{0,i,j} <- if matrix.{i,j}<max_int && i!=j then i else max_int;
			done
		done;

		(* compute *)
		for k = 0 to n-1 do
			for i = 0 to n-1 do
				for j = 0 to n-1 do
					(* new distances *)
					let d_ij = dist.{!last,i,j} in
					let d_ik = dist.{!last,i,k} in
					let d_kj = dist.{!last,k,j} in
					let sum = if d_ik=max_int || d_kj=max_int then max_int else d_ik + d_kj in
					let d_min = min d_ij sum in
					dist.{1-(!last),i,j} <- d_min;

					(* new prior nodes *)
					if d_ij <= sum then
                	prior.{1-(!last),i,j} <- prior.{!last,i,j}
               else
                	prior.{1-(!last),i,j} <- prior.{!last,k,j}
				done
	   	done;
			last := 1-(!last); (* swap between 0 and 1 *)
			(*print n prior last;*)
			done;
			print n dist last;
   	end;;


	(* given a sequence of states, extract the word w such that the deterministic
	automaton generates this sequence by reading w. We assume that all states
	in the list are distinct. *)
let extract_word (nSigma:int) (delta:int Int2Map.t) (states:int list) =
	let get_letter q q' =
		let rec try_each_letter letter = match letter with
			1 -> 1 (* we assume that the successor can be reached *)
			| a -> if Int2Map.mem (q,a) delta then a else try_each_letter (a-1)
		in
		try_each_letter nSigma
	in
	let rec run (q:int) (states:int list) = match states with
		[] -> []
		| q' :: tl -> (get_letter q q') :: (run q' tl)
	in
	run (List.hd states) (List.tl states);;

(*
	let test =
		begin
			let matrix = Array2.create int c_layout 5 5 in
			let content1 = [| 0; 3; 8; max_int; -4;
									max_int; 0; max_int; 1; 7;
									max_int; 4; 0; max_int; max_int;
									2; max_int; -5; 0; max_int;
									max_int; max_int; max_int; 6; 0 |] in
			let content = [| max_int; 3; 8; max_int; -4;
									max_int; max_int; max_int; 1; 7;
									max_int; 4; max_int; max_int; max_int;
									2; max_int; -5; max_int; max_int;
									max_int; max_int; max_int; 6; max_int |] in
			for i=0 to 4 do
				for j=0 to 4 do
					matrix.{i,j} <- content.(i*5+j)
				done
			done;
      	floyd_warshall 5 matrix;
		end;;
*)
























(* get_sccs computes the sccs of a given graph and returns an array scc:{1..nV}->int
	that maps each vertex to its scc
	* vertices are integers with numbers {1,..,nV}
	* succs maps a vertex to its successors,
	* succsT like succs with respect to the transposed graph *)
type colT = WHITE | GRAY | BLACK
let get_sccs (nV:int) (succs:int->int list) (succsT:int->int list) =
   	(* returns an array of vertices sorted according to decreasing finishing time *)
	let finishing_times =
		let color = Array.make (nV+1) WHITE in  (* neglegt color.[0] *)
		let fin = Array.make (nV+1) 0 in
		let idx = ref nV in
		let rec dfs_visit u =
	 	color.(u) <- GRAY;
	 	List.iter
	 		(fun v -> if color.(v) = WHITE then dfs_visit v)
	 		(succs u);
			fin.(!idx) <- u;
			idx := !idx - 1
		in
		for i=1 to nV do
			if color.(i) = WHITE then dfs_visit i
		done;
		fin
	in
	(* returns
		1. the number of sccs found
		2. an array scc:int -> int that maps vertices to its scc *)
	let compute_sccs =
		let scc = Array.make (nV+1) 0 in
		let idx = ref 0 in
		let color = Array.make (nV+1) WHITE in  (* neglegt color.[0] *)
		let rec dfs_visit u =
	 	color.(u) <- GRAY;
	 	List.iter
	 		(fun v -> if color.(v) = WHITE then dfs_visit v)
	 		(succsT u);
	 	scc.(u) <- !idx;  (* store vertex u in the idx-th scc *)
		in
		let fin = finishing_times in
		for i=1 to nV do
			let j = fin.(i) in  (* j is the vertex with the i-th finishing time *)
			if color.(j) = WHITE then begin
	        	idx := !idx + 1;  (* start a new scc *)
				dfs_visit j;
			end
		done;
		(!idx, scc);
	in
	compute_sccs
	
	
	(* topological sort of a graph E = ({1,..,nV}, edges) and returns
		1. an array: vertex -> position with the ordering positions
		2. an array: vertex -> successor vertices as list *)
		let topo_sort (nV:int) (succs:int->int list) =
	   	(* returns an array of vertices sorted according to decreasing finishing time *)
	let finishing_times =
		let color = Array.make (nV+1) WHITE in  (* neglegt color.[0] *)
		let fin = Array.make (nV+1) 0 in
		let idx = ref nV in
		let rec dfs_visit u =
	 	color.(u) <- GRAY;
	 	List.iter
	 		(fun v -> if color.(v) = WHITE then dfs_visit v)
	 		(succs u);
			fin.(!idx) <- u;
			idx := !idx - 1
		in
		for i=1 to nV do
			if color.(i) = WHITE then dfs_visit i
		done;
		fin
	in
finishing_times;;
